$\forall$$T$:Type, ${\it as}$, ${\it as'}$, ${\it bs}$, ${\it cs}$:$T$ List.
\\[0ex]$\parallel$${\it as}$$\parallel$ $=$ $\parallel$${\it as'}$$\parallel$ $\in$ $\mathbb{Z}$ $\Rightarrow$ (${\it cs}$ @ ${\it as}$) $=$ (${\it bs}$ @ ${\it as'}$) $\in$ $T$ List $\Rightarrow$ ${\it cs}$ $=$ ${\it bs}$